MIME-Version: 1.0
Server: CERN/3.0
Date: Wednesday, 20-Nov-96 20:17:33 GMT
Content-Type: text/html
Content-Length: 5082
Last-Modified: Tuesday, 08-Oct-96 17:29:17 GMT

<HEAD>
<TITLE>CS611:  Semantics of Programming Languages</TITLE>
</HEAD>
<BODY>
<h1> <!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><img align=center src="http://www.cs.cornell.edu/Info/Courses/Current/CS611/lambdahead.gif">CS 611:  Semantics of Programming Languages</h1>

<h2> Contents: </h2>
<ul>
<li><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><a href="#Description">Description, Texts, and Prerequisites</a>
<li><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/handouts.html">Handouts</a>
<li><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/lectures.html">Scribed Lecture Notes</a>
<li><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/homework.html">Homework Assignments</a>
<li><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><a href="#Administrivia">Contact Information</a>
<li><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><a href="#Weblinks">Relevant Web Links</a>
</ul>

<a name = "Description">
<h2> Description: </h2>
<p>
<dl>
<dt> <strong>Lectures:</strong>  MWF, 10:10-11:00am, Upson 211
</dl>
<p>
Though CS611 is called ``Advanced Programming Languages'' in the course book,
it is better entitled ``Semantics of Programming Languages''.  The goal
of this course is not to conduct a broad survey of hi-tech programming
languages like C++, Java, or SML, nor to directly study implementation 
mechanisms for these languages (e.g., compressed dispatch tables for multiple
inheritance).  Rather, the goal of this course is to study 
<i>the principles
of formal notation for describing computations, and tools for analyzing 
and proving properties of computations</i>.  These concerns subsume the
study of specific programming languages or implementation mechanisms 
and hence lead to a deeper understanding of programming, specification,
logic, mathematics, and proof theory.  
<p>
For example, we will study notations for abstractly specifying <i>how</i>
programs compute (operational semantics), as well as
notations for describing <i>what</i> programs compute 
(denotational semantics).  In turn, the abstract but precise
realization of these notations will allow us to study techniques 
(induction, logical relations) for
formally proving interesting and relevant properties of 
programming languages (e.g., type safety or compiler correctness).  
<p>
Ideally, a student coming out of this course will have learned something
about how to make informal concepts and notation precise, and how to
manipulate the notation to demonstrate useful properties.  
<p>

<h2> Textbooks: </h2>
<p>
<ul>
<li> <i> Semantics of Programming Languages </i>,  Carl A. Gunter.
<li> <i> ML for the Working Programmer (Second Edition) </i>, Larry Paulson.
</ul>

<h2> Prerequisites: </h2>
<p>
On the programming side, 
we assume experience with at least a Pascal- or C-like language.
Preferably, students will have some knowledge and experience working with
a functional language, such as Scheme, ML, or Haskell.  
<p>
On the theoretical side, we assume a basic proficiency in undergraduate
mathematics, logic, and computer science.  A basic knowledge of 
computability (e.g., turing machines, recursive functions) and
logic (e.g., predicate calculus), as well as some mathematical
maturity is required.  
<p>
This course is designed for PhD students in CS, Math,
OR, and EE.  It is not for MEng or undergraduate students.  If you are an
MEng or undergraduate student, you must talk to the instructor to find out if
the course is suitable for you.  
<p>

<a name = "Administrivia">
<h2> Contact Information: </h2>
<dl>
<dt> <strong>Newsgroup:</strong> <!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><a href="news://cornell.class.cs611">cornell.class.cs611</a>
</dl>
<p>
<dl>
<dt> <strong>Instructor:</strong>  <!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><a href="http://www.cs.cornell.edu/Info/People/jgm/home.html">Greg Morrisett</a>, Upson 4105C, <!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><a href="mailto:jgm@cs.cornell.edu">jgm@cs.cornell.edu</a>, 5-3009
<dt> <strong>Office Hours:</strong>  MF after class or by appointment.
<dt> <strong>Admin. Assistant:</strong>  Linda Competillo, Upson 4115
</dl>
<p>
<dl>
<dt> <strong>TA</strong>:  
     <!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><a href="http://www.cs.cornell.edu/Info/People/ulfar/">&Uacute;lfar 
     Erlingsson</a>, Upson 4162, 
<!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><a href="mailto:ulfar@cs.cornell.edu">ulfar@cs.cornell.edu</a>, 5-2219
<dt> <strong>Office Hours:</strong> Tue 2-3pm, Thu 1:30-2:30pm
</dl>

<a name = "Weblinks">
<h2>Relevant Web Links:</h2>
<ul>
<li> Mark Leone's <!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><a href="http://foxnet.cs.cmu.edu/people/mleone/language-research.html">Resources for Programming Language Research</a>.

<li>Emacs mode for ML:
<ul>
<li> <!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/lib/ml.el">ml.el</a>
<li> <!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/lib/comint.el">comint.el</a> (needed by ml.el)
</ul>

<li>The Fox project's on-line information about <!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><a href="http://foxnet.cs.cmu.edu/sml.html">Standard ML</a>.

<li>Reference information for SML/NJ (postscript):
<ul>
<li> <!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/doc/manual/GUIDE.ps">User's guide</a>
<li> <!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/doc/manual/BASE.ps">Description of the base environment</a>
<li> <!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/doc/manual/SYS.ps">Description of the system environment</a>
<li> <!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/doc/manual/LIB.ps">Library documentation</a>
<li> <!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/doc/manual/TOOL.ps">Documentation of available tools</a>
<li> <!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/doc/manual/index.ps">Reference index<!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><a href="http://www.cs.cornell.edu/Info/Courses/Current/CS611/doc/manual/TOOL.ps">Documentation of available tools</a></a>
</ul>

<li>A gentle <!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><a href="http://fas.sfu.ca/cs/LocalDoc/Software/ML/giml/manual.html">introduction</a> to SML, <i> Andrew Cumming </i>.

<li>MIT's <!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><a href="http://www.ai.mit.edu/!info/sml/!!first">info</a> on SML/NJ.

</ul>


</BODY>
